Nuprl Lemma : es-first-init
11,40
postcript
pdf
es
:event_system{i:l},
e
:es-E(
es
). sqequal(es-first(
es
; es-init(
es
;
e
)); tt)
latex
Definitions
event_system{i:l}
,
t
T
,
x
:
A
.
B
(
x
)
,
es-E(
es
)
,
tt
,
es-first(
es
;
e
)
,
<
a
,
b
>
,
,
s
=
t
,
guard(
T
)
,
P
Q
,
sq_type(
T
)
,
sqequal(
s
;
t
)
,
x
:
A
B
(
x
)
,
b
,
wellfounded{i:l}(
A
;
x
,
y
.
R
(
x
;
y
))
,
t
.1
,
False
,
A
,
Id
,
es-causl(
es
;
e
;
e'
)
,
P
Q
,
es-locl(
es
;
e
;
e'
)
,
do-apply(
f
;
x
)
,
x
:
A
B
(
x
)
,
P
Q
,
Unit
,
left
+
right
,
es-init(
es
;
e
)
,
x
.
t
(
x
)
,
P
Q
,
decidable(
P
)
,
P
Q
Lemmas
decidable
assert
,
es-locl-wellfnd
,
can-apply-pred?
,
eqtt
to
assert
,
eqff
to
assert
,
iff
transitivity
,
not
functionality
wrt
iff
,
assert
of
bnot
,
do-apply
wf
,
do-apply-pred?
,
es-pred-locl
,
bool
sq
,
es-E
wf
,
event
system
wf
origin
es:event_system{i:l}, e:es-E(es). sqequal(es-first(es; es-init(es;e)); tt) es:event_system{i:l}, e:es-E(es). sqequal(es-first(es; es-init(es;e)); tt) 
T
Q
B(x)
b
A
Q
B(x)
x. t(x)
Q